\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Definition} \coqdocvar{Update}(\coqdocvar{st}: \coqdocvar{State})(\coqdocvar{id}: \coqdocvar{Id})(\coqdocvar{val}: \coqdocvar{Val}) : \coqdocvar{State} :=\coqdoceol
\coqdocindent{1.00em}
\coqdockw{fun} (\coqdocvar{id'}: \coqdocvar{Id}) \ensuremath{\Rightarrow} \coqdockw{if} (\coqdocvar{equal\_id} \coqdocvar{id} \coqdocvar{id'}) \coqdockw{then} \coqdocvar{Some} \coqdocvar{val} \coqdockw{else} \coqdocvar{st} \coqdocvar{id'}.\coqdoceol
\end{coqdoccode}